es:ES, ff:FIFO, f2f+:F2F+-decls, e:E, sndr, rcvr:ff.C.
[e: rcvr is_ack  sndr]  (loc(e) = rcvr  Id) 

latex

Definitions	loc(e), <a, b>, Id, s = t, x:A. B(x), b, Void, x:AB(x), P  Q, False, A, x:A  B(x), ES, FIFO, F2F+-decls, t.1, E, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), ff.C, f(a), [e: i p j], @i(x:T), Dec(P), let x,y = A in B(x;y), P & Q, P  Q, A r B, {T}, isrcv(e), t  T, Atom$n, Type, P  Q, ff.R, A c B, is_ack
Lemmas	rcv-it wf, f2f+Ack wf, fifoC wf, es-E wf, F2F+-decls wf, FIFO wf, event system wf, f2f+-property, es-isrcv-loc, equal functionality wrt subtype rel, es-loc-pred